Hilbert space

Definition

A Hilbert space is a vector space $H$ with inner product $\langle f,g \rangle$ such that the norm defined by $\lvert f \rvert = \sqrt{\langle f,f \rangle}$ turns $H$ into a complete metric space

(i.e. complete inner product space, whereas an inner product space may be known as a pre-Hilbert space)

A Hilbert space is a complete normed inner product space.

@[variable_alias]
structure HilbertSpace (𝕜 E : Type*) [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]

(RCLike: real $\mathbb{R}$ or complex $\mathbb{C}$ , NormedAddCommGroup: normed group, InnerProductSpace: extension of NormedSpace and Inner inner product, CompleteSpace: complete metric space)

examples:
- real numbers $\mathbb{R}^n$ with $\langle v,u \rangle$ vector dot product of $v$ and $u$